perm filename A72.TEX[254,RWF] blob sn#863866 filedate 1988-11-17 generic text, type C, neo UTF8
COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	\input macro[1,mps]
C00010 ENDMK
C⊗;
\input macro[1,mps]
\magnification\magstephalf
\baselineskip 14pt
\leftline{\sevenrm A72.Tex[254,mps]\today}
\leftline{\copyright\sevenrm Robert W. Floyd, November 14, 1988}
\leftline{\sevenrm Unpublished Draft}
\bigskip
\noindent{\bf Undecidability of First-order Predicate Calculus}
\bigskip
Let $M$ be an oblivious two-counter Turing machine.  The halting
problem for $M$ is undecidable, even when restricted to deterministic
programs.  We will construct, from any standardized program $P$ for $M$, a
formula in the first-order predicate calculus that is provable if and
only if $P$ has a computation (``halts'').  This reduces the halting
problem to the problem of provability in the FPC, so the latter is
undecidable.

As an example, take this program, $P↓1$, for a one-counter machine:
\vskip 1in
The formula we construct is:
$$\eqalign {f↓1(0) &\land (f↓1(x)\supset f↓2 (S(x)))\land
(f↓2(x)\supset f↓3 (S(x)))\cr
&\land (f↓3 (S(x))\supset f↓3(x))\land (f↓3(0)\supset
f↓4(0)) \supset f↓4(0).\cr}$$
By the deduction theorem, this formula is provable iff $f↓4(0)$ is provable
from the hypotheses 
\smallskip
\halign{\qquad # \hfil & \quad # \hfil\cr
$(H↓1): $&$ f↓1(0),$\cr
$(H↓2): $&$ f↓1(x) \supset f↓2 \left(S(x)\right)$,\cr
$(H↓3): $&$ f↓2(x) \supset f↓3\left (S(x)\right)$,\cr
$(H↓4): $&$ f↓3\left (S(x)\right)\supset f↓3(x),\hbox{ and }$\cr
$(H↓5): $&$ f↓3(0) \supset f↓4(0).$\cr}
\smallskip
\noindent The proof is
\smallskip
\halign{\qquad # \hfil & \quad  # \hfil \cr
$f↓2\left (S(0)\right)$&$(H↓1, H↓2)$\cr
$f↓3\left (S\left (S(0)\right )\right )$&$(\hbox {above}, H↓3)$\cr
$f↓3\left(S(0)\right)$&$(\hbox {above}, H↓4)$\cr
$f↓3(0)$&$(\hbox {above}, H↓4)$\cr
$f↓4(0)$&$(\hbox {above}, H↓5)$\cr}
\smallskip
If we interpret $S(x)$ as $x+1$ in the natural numbers, and $f↓i(x)$ as the
proposition that the configuration $\langle i,x\rangle$ occurs in the
computation of $P↓1$, the above proves that $\langle 1,0\rangle$, $\langle 2,1
\rangle$, $\langle 3,2\rangle$, $\langle 3,1\rangle$, $\langle 3,0\rangle$, and
$\langle 4,0\rangle$ are configurations that occur.  By induction on the
number of the steps where a configuration occurs, we can prove
$f↓i(x)$ for any $\langle i,x\rangle$ that does occur, and in particular can 
prove the occurrence of the standard halting configuration if it occurs.  So,
if $P↓1$ halts, the formula is provable.  If $P↓1$ doesn't halt, though, the
hypotheses are all true but the conclusion is false in the intended
interpretation, and the soundness of the  FPC guarantees that one can't prove 
false conclusions from true hypotheses.  So the formula is provable iff
$P↓1$ halts.

The general rule for constructing a formula from a program $P$ is:
\medskip

If $q↓i$ is the initial control state, $f↓i(0,0)$ is a hypothesis.

If $\langle i→j,{\it incr\, ctr}1\rangle$ is an instruction, 
$f↓i(x,y) \supset f↓j(S(x),y)$ is a hypothesis.

If $\langle i→j,{\it incr\, ctr}2\rangle$ is an instruction, 
$f↓i(x,y) \supset f↓j(x,S(y))$ is a hypothesis.

If $\langle i→j, {\it decr\, ctr}1\rangle$ is an instruction, 
$f↓i(S(x), y) \supset f↓j(x,y)$ is a hypothesis.

If $\langle i→j, {\it decr\, ctr}2\rangle$ is an instruction, 
$f↓i(x, S(y)) \supset f↓j(x,y)$ is a hypothesis.

If $\langle i→j, {\it ctr}1=0\rangle$ is an instruction, 
$f↓i (0,y)\supset f↓j(0,y)$ is a hypothesis.

If $\langle i→j, {\it ctr}2=0\rangle$ is an instruction, 
$f↓i(x,0) \supset f↓j(x,0)$ is a hypothesis.

If $q↓i$ is the single accepting control state, $f↓i(0,0)$ is the conclusion.
\medskip

The formula constructed then states that the conjunction of all the hypotheses
implies the conclusion.  (Some technical points:  A corresponding formula
for resolution proofs would simply change $f↓i(x,y) \supset f↓j(S(x), y)$ to
$\overline {f↓i(x,y)} \lor f↓j(S(x), j)$, and form the conjunction of the
hypotheses with the negation of the conclusion.  The Herbrand universe of the
formulas is $\{0, S(0), S(S(0)),\ldots\}$, isomorphic to $\{0,1,2,\ldots\}$,
with $S(x)$ corresponding to $x+1$.)

We have shown how to construct from any halting problem a formula in the FPC
that is provable iff the program in question halts.  Therefore provability
in the FPC is not decidable; the set of provable formulas is not recognized by
any TM program.  The set is accepted by a TM (that tries every possible
proof until one succeeds) so we know by [?] theorem that the complementary
set is not accepted by any TM program.  The complementary set, the unprovable
formulas of the FPC, are known to be the same as the invalid formulas, the
formulas that can be interpreted in a way that makes them false.
\end